package krao.reformulation;

import java.util.ArrayList;

import krao.data.Atom;
import krao.data.ClassAtom;
import krao.data.ConjQuery;
import krao.data.RoleAtom;
import krao.data.TBox;
import krao.data.TBoxClass;
import krao.data.TBoxProperty;
import krao.data.UnionConjQuery;

import org.apache.log4j.Logger;

/**
 * Class responsible for performing the PerfectRef algorithm, which effectively
 * encodes TBox assertions into given query.
 * 
 * @author Pepe
 * 
 */
public class Reformulator {
	private final static Logger logger = Logger.getLogger(Reformulator.class);

	//@formatter:off
	/*
	 * Algorithm taken from 
	 * Tractable Reasoning and Efficient Query Answering in Description Logics: 
	 * The DL-Lite Family
	 * Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, 
	 * Maurizio Lenzerini, Riccardo Rosati
	 * calv-etal-JAR-2007.pdf 30 5.1 Query Reformulation 
	 
	An argument of an atom in a query is bound if it corresponds 
	to either a distinguished variable or a shared variable, that is, a variable
	occurring at least twice in the query body, or a constant. 
	
	An argument of an atom in a query is unbound if it corresponds to a
	nondistinguished nonshared variable = symbol ‘_’

	A PI I is applicable to an atom A(x) if I has A in its right-hand side. 
	A PI I is applicable to an atom P(x1, x2) if 
		(1) x2 = _ and the right-hand side of I is exist P; or 
		(2) x1 = _ and the right-hand side of I is exist P−; or 
		(3) I is a role inclusion assertion and its right-hand side is either P or P−. 
		
	An inclusion I is applicable to an atom g 
		if the predicate of g is equal to the predicate in the right-hand side of I 
		and, in the case when I is an inclusion assertion between concepts, 
		if g has at most one bound argument and corresponds to the object 
		that is implicitly referred to by the inclusion I. 
		
		We indicate with gr(g, I) the atom obtained from the atom g 
		by applying the applicable inclusion I. */
	
	/*
	 * Algorithm PerfectRef (q, )
		Input: conjunctive query q, TBox
		Output: union of conjunctive queries PR
		
		PR := {q};
		repeat
			PR := PR;
			for each q PR do
				(a) for each g in q do
						for each PI I in do
							if I is applicable to g
								then PR := PR {q[g/gr(g, I)]}
				(b) for each g1, g2 in q do
						if g1 and g2 unify
							then PR := PR {τ (reduce(q, g1, g2))};
		until PR = PR ;
		return PR
	 */
	//@formatter:on
	/**
	 * Method takes ucq and a tbox and using PerfectRef algorithm, it
	 * reformulates ucq.
	 * 
	 * @param ucq
	 *            Union of conjunctive queries, which will be reformulated
	 * @param tbox
	 *            tbox used in PerfectRef algorithm reformulation
	 * @return
	 */
	public static void reformulateQuery(UnionConjQuery ucq, TBox tbox) {
		if (tbox == null) {
			throw new IllegalArgumentException("TBox was not initialized");
		}
		logger.debug("Reformulating queries in ucq:\n" + ucq.toStringQueryForm());
		// start with the only query we have
		ucq.anonymize();
		UnionConjQuery newQueries = new UnionConjQuery();
		boolean changed = true;
		// while there are some changes in the UCQ in cycle run
		while (changed) {
			// store new queries here
			newQueries.clear();

			for (final ConjQuery oneQuery : ucq.getQueries()) {
				for (final Atom atom : oneQuery.getBody()) {
					ArrayList<Atom> newAtoms = getNewAtomsFromTBox(atom, tbox);
					if (newAtoms != null) {
						for (Atom newAtom : newAtoms) {
							newQueries.addQuery(replace(oneQuery, atom, newAtom));
						}
					}
				}
			}
			changed = ucq.mergeIn(newQueries);
		}
		ucq.removeInvalidQueries();
	}

	private static ConjQuery replace(final ConjQuery oneQuery, final Atom oldAtom,
			final Atom newAtom) {
		// create new query
		ConjQuery newQuery = oneQuery.clone();
		// replace the old atom with a new one in the new query
		newQuery.replace(oldAtom, newAtom);
		// reduce
		newQuery.reduce();
		// logger.info(newQuery.toString());
		// return the new query
		return newQuery;
	}

	/**
	 * Returns the list of atoms created from the tbox and original atom.
	 * 
	 * @param atom
	 *            atom to be reformulated
	 * @param tbox
	 *            tbox used in reformulation
	 * @return list of new atoms (subclasses of class from original atom)
	 */
	private static ArrayList<Atom> getNewAtomsFromTBox(Atom atom, TBox tbox) {
		ArrayList<Atom> result = new ArrayList<Atom>();
		// atom == ClassAtom
		if (atom.isClassAtom()) {
			if (tbox.containsClass(atom.getName())) {
				TBoxClass thisClass = tbox.getClass(atom.getName());
				// case 1
				for (String oneClass : thisClass.getSubClasses()) {
					Atom newAtom = (Atom) atom.clone();
					newAtom.setName(oneClass);
					result.add(newAtom);
				}
				// case 2
				for (TBoxProperty oneClass : thisClass.getDomainOf()) {
					Atom newAtom = new RoleAtom(oneClass.getName(), atom.getFirstArg(),
							null);
					result.add(newAtom);
				}
				// case 3
				for (TBoxProperty oneClass : thisClass.getRangeOf()) {
					Atom newAtom = new RoleAtom(oneClass.getName(), null,
							atom.getFirstArg());
					result.add(newAtom);
				}
				return result;
			}
			return null;
		} else {
			// atom == RoleAtom
			if (tbox.containsProperty(atom.getName())) {
				TBoxProperty thisProp = tbox.getProperty(atom.getName());
				if (atom.getFirstArg() == null) {
					if (atom.getSecondArg() == null) {
						// nothing to do here
					} else {

						// P(_, x)
						// case 7
						for (TBoxClass oneClass : thisProp.getRange()) {
							Atom newAtom = new ClassAtom(oneClass.getName(),
									atom.getSecondArg());
							result.add(newAtom);
						}
						// case 8
						// N/A inverse role hierarchies

						// case 9
						// N/A inverse role hierarchies
					}
				} else {
					// first arg != null
					if (atom.getSecondArg() == null) {
						// P(x, _)
						// case 4
						for (TBoxClass oneClass : thisProp.getDomain()) {
							Atom newAtom = new ClassAtom(oneClass.getName(),
									atom.getFirstArg());
							result.add(newAtom);
						}

						// case 5
						// N/A role hierarchies

						// case 6
						// N/A role hierarchies
					} else {
						// first arg != null, second arg != null
						// P(x,y)
						// case 10
						for (String oneSubProp : thisProp.getSubProperties()) {
							Atom newAtom = (Atom) atom.clone();
							newAtom.setName(oneSubProp);
							result.add(newAtom);
						}

						// case 11
						for (String oneInvProp : thisProp.getInverseProp()) {
							Atom newAtom = (Atom) atom.clone();
							newAtom.setName(oneInvProp);
							String argTmp = newAtom.getFirstArg();
							newAtom.setFirstArg(newAtom.getSecondArg());
							newAtom.setSecondArg(argTmp);
							result.add(newAtom);
						}
					}

				}
				return result;
			}
			return null;
		}
	}
}
